module traveldream/pacchetti

open traveldream/prodotti
open util/integer

/* Assumiamo qui che nelle date l'ordine di grandezza di nostro
 * interesse sia dei giorni e che essi siano semplicemente
 * incrementati da 0 a partire da un dato momento (come il timestamp).
 * Questo permette di modellare correttamente i concetti in alloy
 * senza dover introdurre il mantenimento di coerenza
 * di un calendario. */
sig Data in Int {} {
	this >= 0
}

one sig Oggi in Data {}

sig Durata in Int {} {
	this >= 1
}

sig Giorno in Int {} {
	this >= 0
}

abstract sig Pacchetto {
	luogo : one Luogo,
	andata : one Trasporto,
	soggiorno : one Alloggio,
	programma : set (Attivita lone -> lone Giorno)
	durata : one Durata,
	ritorno : one Trasporto
} {
	/* Coerenza del luogo di svolgimento del viaggio */
	luogo = (andata.destinazione + soggiorno.luogo + attivita.luogo + ritorno.provenienza)
	/* I giorni di attività sono interni ad arrivo e partenza */
	all giorno : programma[Attivita] | giorno > 0 and giorno < durata
}

sig PacchettoPredefinito extends Pacchetto {} {
	/* Coerenza del luogo di partenza e di rientro */
	andata.provenienza = ritorno.destinazione
}

sig PacchettoPersonalizzato extends Pacchetto {
	modello : one PacchettoPredefinito,
	data : one Data
} {
	/* Il viaggio si svolge sempre nello stesso luogo del modello */
	luogo = modello.@luogo
}

pred equivalente [p1, p2 : Pacchetto] {
	p1.luogo = p2.luogo
	p1.andata = p2.andata
	p1.soggiorno = p2.soggiorno
	p1.programma.Giorno = p2.programma.Giorno
	p1.durata = p2.durata
	p1.ritorno = p2.ritorno
}

pred identico [p1, p2 : PacchettoPredefinito] {
	equivalente[p1, p2]
	p1.programma = p2.programma
}

pred identico [p1, p2 : PacchettoPersonalizzato] {
	equivalente[p1, p2]
	p1.modello = p2.modello
	p1.data = p2.data
	p1.programma = p2.programma
}

pred scaduto [p : PacchettoPersonalizzato] {
	/* Il viaggio non deve iniziare nel passato */
	p.data <= Oggi
}

pred contenuto [p : Pacchetto, s : set Prodotto] {
	(p.andata + p.soggiorno + p.programma.Giorno + p.ritorno) in s
}

/* Esempio di pacchetto personalizzato comune */
pacchettoComune: run {
	some p : PacchettoPersonalizzato {
		some p.programma
		p.andata.provenienza = p.ritorno.destinazione
	}
} for 10

/* Esempio pacchetto di base generato dal sistema quando se ne personalizza uno predefinito */
pacchettoBase: run {
	some p : PacchettoPersonalizzato {
		equivalente[p, p.modello]
		p.programma = p.modello.programma
		p.data = 0
	}
} for 10

/* Esempio di eliminazione di un'attività */
eliminaAttivita: run {
	some p, p' : PacchettoPersonalizzato {
		p.andata = p'.andata
		p.soggiorno = p'.soggiorno
		one a : p.programma {
			p.programma - a = p'.programma
		}
		p.ritorno = p'.ritorno
		p.modello = p'.modello
		p.data = p'.data
		p.durata = p'.durata
	}
} for 10

/* Non si possono fare più di una attività nello stesso giorno */
unaAttivitaPerGiorno: check {
	no p : PacchettoPersonalizzato {
		some disj a1, a2 : p.programma.Giorno | p.programma[a1] = p.programma[a2]
	}
} for 10

/* Per poter fare tutte le attività il viaggio deve durare abbastanza */
durataMinimaViaggio: check {
	no p : PacchettoPersonalizzato {
		p.durata < (#p.attivita + 1)
	}
} for 10
